$\forall$${\it es}$:ES\{i\}, $i$:Id, $L$:IdLnk List, $T$:(Id$\rightarrow$Type$_{\mbox{\scriptsize i}}$). \\[0ex]es{-}secret{-}server\{table:ut2, encrypt:ut2, decrypt:ut2\}(${\it es}$; $T$; $L$; $i$) $\in$ Prop$_{\mbox{\scriptsize i'}}$